import java.util.Scanner;

public class Main {

	static boolean TRACE = false;
	// false if you don't want detailed printing
	
	

	public static void main(String[] args) {

		Scanner s = new Scanner(System.in);
		System.out.println("Enter 1: if you want to unify two FOL expressions");
		System.out
				.println("Enter 2: if you want transform a FOL expression to its CLAUSE FORM");
		int choice = Integer.parseInt(s.nextLine());

		if (choice == 1) {
			System.out
					.println("Enter 1: if you want unify 'p(x,g(x),g(f(A)))' with 'p(f(u),v,v)' ");
			System.out
					.println("Enter 2: if you want unify 'p(A,y,f(y))' with 'P(z,z,u)' ");
			System.out
					.println("Enter 3: if you want unify 'f(x,g(x),x)' with 'f(g(u),g(g(z)),z)' ");
			System.out.println("Enter 4: if you want to enter a new test case");
			int testCase = Integer.parseInt(s.nextLine());
			if (testCase == 1)
				Unification.unify("p(x,g(x),g(f(A)))", "p(f(u),v,v)");
			else if (testCase == 2)
				Unification.unify("p(A,y,f(y))", "p(z,z,u)");
			else if (testCase == 3)
				Unification.unify("f(x,g(x),x)", "f(g(u),g(g(z)),z)");
			else if (testCase == 4) {
				System.out.println("Enter the first sentence");
				String s1 = s.nextLine();
				System.out.println("Enter the second sentence");
				String s2 = s.nextLine();
				Unification.unify(s1, s2);
			}
			System.out.println("{" + Unification.theta + "}");
		} else {

			System.out
					.println("Enter 1: if you want CNF: VxEy[P(x,y) & VxEy[Q(x,y) - ~P(x)]]");
			System.out
					.println("Enter 2: if you want CNF: Vx[P(x) = (Q(x) & Ey[Q(y) & R(y,x)])]");
			System.out
					.println("Enter 3: if you want CNF: 'Vx[P(x) = (Q(x) & Ey[Q(y) & R(y, x)])]");
			System.out.println("Enter 4: if you want to enter a new test case");
			int testCase = Integer.parseInt(s.nextLine());

			String input = "";
			if (testCase == 1)
				input = "VxEy[P(x,y) & VxEy[Q(x,y) - ~P(x)]]";
			else if (testCase == 2)
				input = "Vx[P(x) = (Q(x) & Ey[Q(y) & R(y,x)])]";
			else if (testCase == 3)
				input = "Vx[P(x) = (Q(x) & Ey[Q(y) & R(y, x)])]";
			else {
				if (testCase == 4) {
					System.out.println("Enter the first sentence");
					input = s.nextLine();
				}
			}

			ClauseForm.convertToCNF(input, TRACE);

		}

	}
}
